g:IMonoid, a:|g|. (a * e) = a & (e * a) = a 

latex

Up	groups 1
Definitions of Statement	IsMonoid(T;op;id), IMonoid
Definitions	t  T, x:A. B(x), IMonoid, P & Q, IsMonoid(T;op;id), Ident(T;op;id)
Lemmas	imon wf, imon properties